#include "MiniSat.h"
#include "Sort.h"
#include <cmath>


namespace MiniSat {
//=================================================================================================
// Debug:


// For derivation output (verbosity level 2)
#define L_IND    "%-*d"
#define L_ind    decisionLevel()*3+3,decisionLevel()
#define L_LIT    "%sx%d"
#define L_lit(p) sign(p)?"~":"", var(p)

// Just like 'assert()' but expression will be evaluated in the release version as well.
inline void check(bool expr) { assert(expr); }


//=================================================================================================
// Helpers:


void removeWatch(vec<LitClauseUnion>& ws, LitClauseUnion elem)
{
    int j = 0;
    for (; ws[j] != elem  ; j++) assert(j < ws.size());
    for (; j < ws.size()-1; j++) ws[j] = ws[j+1];
    ws.pop();
}


//=================================================================================================
// Operations on clauses:

// Returns FALSE if top-level conflict detected (must be handled); TRUE otherwise.
// 'out_clause' may be set to NULL if clause is already satisfied by the top-level assignment.
//
bool Solver::newClause(const vec<Lit>& ps_, bool learnt, Clause*& out_clause)
{
    //for (int i = 0; i < ps_.size(); i++)
    //    printf(L_LIT" ", L_lit(ps_[i]));
    //printf("\n");
    vec<Lit>    qs;
    if (&out_clause != NULL) out_clause = NULL;

    if (!learnt){
        assert(decisionLevel() == 0);
        ps_.copyTo(qs);             // Make a copy of the input vector.

        // Remove false literals:
        for (int i = 0; i < qs.size();){
            if (value(qs[i]) != l_Undef){
                if (value(qs[i]) == l_True)
                    return true;    // Clause always true -- don't add anything.
                else
                    qs[i] = qs.last(),
                    qs.pop();
            }else
                i++;
        }

        // Remove duplicates:
        sortUnique(qs);
        for (int i = 0; i < qs.size()-1; i++){
            if (qs[i] == ~qs[i+1])
                return true;        // Clause always true -- don't add anything.
        }
    }
    const vec<Lit>& ps = learnt ? ps_ : qs;     // 'ps' is now the (possibly) reduced vector of literals.

    if (ps.size() == 0)
        return false;
    else if (ps.size() == 1)
        return enqueue(ps[0]);
    else{
        // Allocate clause:
        assert(sizeof(Lit)   == sizeof(unsigned));
        assert(sizeof(float) == sizeof(unsigned));
        void*   mem = xmalloc<char>(sizeof(Clause) + sizeof(unsigned)*(ps.size() + (int)learnt));
        Clause* c   = new (mem) Clause(learnt,ps);

        // For learnt clauses only:
        if (learnt){
            // Put the second watch on the literal with highest decision level:
            int     max_i = 1;
            int     max   = level[var(ps[1])];
            for (int i = 2; i < ps.size(); i++)
                if (level[var(ps[i])] > max)
                    max   = level[var(ps[i])],
                    max_i = i;
            (*c)[1]     = ps[max_i];
            (*c)[max_i] = ps[1];

            // Bumping:
            claBumpActivity(c); // (newly learnt clauses should be considered active)
            for (int i = 0; i < ps.size(); i++)
                varBumpActivity(ps[i]);

            stats.learnts++;
            stats.learnts_literals += c->size();
        }else{
            stats.clauses++;
            stats.clauses_literals += c->size();
        }

        // Store clause:
        if (c->size() == 2){
            watches[index(~(*c)[0])].push(makeLit((*c)[1]));
            watches[index(~(*c)[1])].push(makeLit((*c)[0]));
        }else{
            watches[index(~(*c)[0])].push(makeClause(c));
            watches[index(~(*c)[1])].push(makeClause(c));
        }
        if (&out_clause != NULL) out_clause = c;

        return true;
    }
}


void Solver::remove(Clause* c, bool just_dealloc)
{
    if (!just_dealloc)
        if (c->size() == 2){
            removeWatch(watches[index(~(*c)[0])], makeLit((*c)[1]));
            removeWatch(watches[index(~(*c)[1])], makeLit((*c)[0]));
        }else{
            removeWatch(watches[index(~(*c)[0])], makeClause(c));
            removeWatch(watches[index(~(*c)[1])], makeClause(c));
        }

    if (c->learnt()){
        stats.learnts--;
        stats.learnts_literals -= c->size();
    }else{
        stats.clauses--;
        stats.clauses_literals -= c->size();
    }

    xfree(c);
}


// Can assume everything has been propagated! (esp. the first two literals are != l_False, unless
// the clause is binary and satisfied, in which case the first literal is true)
// Returns True if clause is satisfied (will be removed), False otherwise.
//
bool Solver::simplify(Clause* c) const
{
    assert(decisionLevel() == 0);
    for (int i = 0; i < c->size(); i++){
        if (value((*c)[i]) == l_True)
            return true;
    }
    return false;
}



//=================================================================================================
// Minor methods:


// Creates a new SAT variable in the solver. If 'decision_var' is cleared, variable will not be
// used as a decision variable (NOTE! This has effects on the meaning of a SATISFIABLE result).
//
Var Solver::newVar(bool dvar)
{
    int     index;
    index = nVars();
    watches .push();          // (list for positive literal)
    watches .push();          // (list for negative literal)
    reason  .push(makeClause(NULL));
    assigns .push(toInt(l_Undef));
    level   .push(-1);
    activity.push(0);
    polarity_sug.push(toInt(l_Undef));
    order   .newVar(dvar);
    analyze_seen.push(0);
    trail.capacity(index+1);
    return index;
}


// Returns FALSE if immediate conflict.
bool Solver::assume(Lit p) {
    //if (verbosity >= 2)
    //printf(L_IND"assume("L_LIT") %g\n", L_ind, L_lit(p), activity[var(p)]);
    trail_lim.push(trail.size());
    return enqueue(p); }


// Revert to the state at given level.
void Solver::cancelUntil(int level) {
    if (decisionLevel() > level){
        for (int c = trail.size()-1; c >= trail_lim[level]; c--){
            Var     x  = var(trail[c]);
            assigns[x] = toInt(l_Undef);
            reason [x] = makeClause(NULL);
            order.undo(x); }
        trail.shrink(trail.size() - trail_lim[level]);
        trail_lim.shrink(trail_lim.size() - level);
        qhead = trail.size(); } }


// Record a clause and drive backtracking. 'clause[0]' must contain the asserting literal.
//
void Solver::record(const vec<Lit>& clause)
{
    assert(clause.size() != 0);
    Clause* c;
    check(newClause(clause, true, c));
    assert(ok);
    check(enqueue(clause[0], makeClause(c)));
    if (c != NULL) learnts.push(c);
}


//=================================================================================================
// Major methods:


#define ANALYZE_LIT(p) \
            if (!seen[var(q)] && level[var(q)] > 0){                \
                varBumpActivity(q);                                 \
                seen[var(q)] = 1;                                   \
                if (level[var(q)] == decisionLevel())               \
                    pathC++;                                        \
                else{                                               \
                    out_learnt.push(q);                             \
                    out_btlevel = max(out_btlevel, level[var(q)]);  \
                }                                                   \
            }
/*_________________________________________________________________________________________________
|
|  analyze : (confl : Clause*) (out_learnt : vec<Lit>&) (out_btlevel : int&)  ->  [void]
|  
|  Description:
|    Analyze conflict and produce a reason clause.
|  
|    Pre-conditions:
|      * 'out_learnt' is assumed to be cleared.
|      * Current decision level must be greater than root level.
|  
|    Post-conditions:
|      * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'.
|  
|  Effect:
|    Will undo part of the trail, upto but not beyond the assumption of the current decision level.
|________________________________________________________________________________________________@*/
void Solver::analyze(Clause* _confl, vec<Lit>& out_learnt, int& out_btlevel)
{
    LitClauseUnion confl = makeClause(_confl);
    vec<char>&     seen  = analyze_seen;
    int            pathC = 0;
    Lit            p     = lit_Undef;

    // Generate conflict clause:
    //
    out_learnt.push();      // (leave room for the asserting literal)
    out_btlevel = 0;
    int index = trail.size()-1;
    do{
        assert(confl != makeClause(NULL));          // (otherwise should be UIP)

        if (confl.isLit()){
            Lit q = confl.getLit();
            ANALYZE_LIT(p);
        }else{
            Clause& c = *confl.getClause();
            if (c.learnt())
                claBumpActivity(&c);

            for (int j = p == lit_Undef ? 0 : 1; j < c.size(); j++){
                Lit q = c[j];
                ANALYZE_LIT(p);
            }
        }

        // Select next clause to look at:
        while (!seen[var(trail[index--])]);
        p     = trail[index+1];
        confl = reason[var(p)];
        seen[var(p)] = 0;
        pathC--;

    }while (pathC > 0);
    out_learnt[0] = ~p;

    /*if (opt_branch_pbvars){ ... <code here Niklas> }*/

  #if 1
    // Simplify conflict clause (a bit more):
    //
    int i,j;
    unsigned int minl = 0;
    for (i = 1; i < out_learnt.size(); i++)
        minl |= 1 << (level[var(out_learnt[i])] & 31);

    out_learnt.copyTo(toclear);
    for (i = j = 1; i < out_learnt.size(); i++)
        if (reason[var(out_learnt[i])] == makeClause(NULL) || !removable(out_learnt[i],minl))
            out_learnt[j++] = out_learnt[i];
  #else
    // Simplify conflict clause (a little):
    //
    int i,j;
    out_learnt.copyTo(toclear);
    for (i = j = 1; i < out_learnt.size(); i++){
        LitClauseUnion r = reason[var(out_learnt[i])];
        if (r == makeClause(NULL))
            out_learnt[j++] = out_learnt[i];
        else if (r.isLit()){
            Lit q = r.getLit();
            if (!seen[var(q)] && level[var(q)] != 0)
                out_learnt[j++] = out_learnt[i];
        }else{
            Clause& c = *r.getClause();
            for (int k = 1; k < c.size(); k++)
                if (!seen[var(c[k])] && level[var(c[k])] != 0){
                    out_learnt[j++] = out_learnt[i];
                    break; }
        }
    }
  #endif

    stats.max_literals += out_learnt.size();
    out_learnt.shrink(i - j);
    stats.tot_literals += out_learnt.size();

    for (int j = 0; j < toclear.size(); j++) seen[var(toclear[j])] = 0;    // ('seen[]' is now cleared)

    //printf(L_IND"Learnt {", L_ind);
    //for (int i = 0; i < out_learnt.size(); i++) printf(" "L_LIT, L_lit(out_learnt[i]));
    //printf(" } at level %d\n", out_btlevel);
}

/* Document me!
 */
#define REMOVABLE_LIT(p) \
            if (!analyze_seen[var(p)] && level[var(p)] != 0)                                             \
                if (reason[var(p)] != makeClause(NULL) && ((1 << (level[var(p)] & 31)) &  minl) != 0){   \
                    analyze_seen[var(p)] = 1;                                                            \
                    stack.push(p);                                                                       \
                    toclear.push(p);                                                                     \
                }else{                                                                                   \
                    for (int j = top; j < toclear.size(); j++)                                           \
                        analyze_seen[var(toclear[j])] = 0;                                               \
                    toclear.shrink_(toclear.size() - top);                                               \
                    return false;                                                                        \
                }

bool Solver::removable(Lit l, unsigned int minl)
{
    assert(reason[var(l)] != makeClause(NULL));
    stack.clear_(); stack.push(l);
    int top = toclear.size();
    while (stack.size() > 0){
        assert(reason[var(stack.last())] != makeClause(NULL));
        LitClauseUnion r = reason[var(stack.last())]; stack.pop();
        if (r.isLit()){
            Lit q = r.getLit();
            REMOVABLE_LIT(q);
        }else{
            Clause& c = *r.getClause();
            for (int i = 1; i < c.size(); i++)
                REMOVABLE_LIT(c[i]);
        }
    }

    return true;
}


/*_________________________________________________________________________________________________
|
|  enqueue : (p : Lit) (from : Clause*)  ->  [bool]
|  
|  Description:
|    Puts a new fact on the propagation queue as well as immediately updating the variable's value.
|    Should a conflict arise, FALSE is returned.
|  
|  Input:
|    p    - The fact to enqueue
|    from - [Optional] Fact propagated from this (currently) unit clause. Stored in 'reason[]'.
|           Default value is NULL (no reason).
|  
|  Output:
|    TRUE if fact was enqueued without conflict, FALSE otherwise.
|________________________________________________________________________________________________@*/
bool Solver::enqueue(Lit p, LitClauseUnion from)
{
    if (value(p) != l_Undef){
        return value(p) != l_False;
    }else{
        //printf(L_IND"bind("L_LIT")\n", L_ind, L_lit(p));
        // New fact -- store it.
        assigns[var(p)] = toInt(lbool(!sign(p)));
        level  [var(p)] = decisionLevel();
        reason [var(p)] = from;
        trail.push_(p);
        return true;
    }
}


/*_________________________________________________________________________________________________
|
|  propagate : [void]  ->  [Clause*]
|  
|  Description:
|    Propagates all enqueued facts. If a conflict arises, the conflicting clause is returned,
|    otherwise NULL.
|  
|    Post-conditions:
|      * the propagation queue is empty, even if there was a conflict.
|________________________________________________________________________________________________@*/
Clause* Solver::propagate(void)
{
    Clause* confl = NULL;
    while (qhead < trail.size()){
        //stats.propagations++;
        Lit                   p  = trail[qhead++];     // 'p' is enqueued fact to propagate.
        vec<LitClauseUnion>&  ws = watches[index(p)];
        LitClauseUnion       *i  = (LitClauseUnion*)ws, *j = i, *end = i + ws.size();

        for (;;) {
        next:
            if (i == end) break;
            if (i->isLit()){
                if (!enqueue(i->getLit(),makeLit(p))){
                    confl = tmp_binary;
                    (*confl)[1] = ~p;
                    (*confl)[0] = i->getLit();

                    qhead = trail.size();
                    // Copy the remaining watches:
                    while (i < end)
                        *j++ = *i++;
                }
                else
                    *j++ = *i++;
            }else{
                Clause& c = *i->getClause(); i++;
                // Make sure the false literal is data[1]:
                Lit false_lit = ~p;
                if (c[0] == false_lit)
                    c[0] = c[1], c[1] = false_lit;

                assert(c[1] == false_lit);

                // If 0th watch is true, then clause is already satisfied.
                Lit   first = c[0];
                lbool val   = value(first);
                if (val == l_True){
                    *j++ = makeClause(&c);
                    goto next;
                }else{
                    // Look for new watch:
                    for (int k = 2; k < c.size(); k++)
                        if (value(c[k]) != l_False){
                            c[1] = c[k]; c[k] = false_lit;
                            watches[index(~c[1])].push(makeClause(&c));
                            goto next; }

                    // Clause is unit under assignment:
                    *j++ = makeClause(&c);
                    if (!enqueue(first, makeClause(&c))){
                        confl = &c;
                        qhead = trail.size();
                        // Copy the remaining watches:
                        while (i < end)
                            *j++ = *i++;
                    }
                }
            }
        }
        //stats.inspects += j - (Clause**)ws;
        ws.shrink_(i - j);
    }

    return confl;
}


/*_________________________________________________________________________________________________
|
|  reduceDB : ()  ->  [void]
|  
|  Description:
|    Remove half of the learnt clauses, minus the clauses locked by the current assignment. Locked
|    clauses are clauses that are reason to a some assignment.
|________________________________________________________________________________________________@*/
struct reduceDB_lt { bool operator () (Clause* x, Clause* y) { return x->size() > 2 && (y->size() == 2 || x->activity() < y->activity()); } };
void Solver::reduceDB(void)
{
    int     i, j;
    double  extra_lim = cla_inc / learnts.size();    // Remove any clause below this activity

    sort(learnts, reduceDB_lt());
    for (i = j = 0; i < learnts.size() / 2; i++){
        if (learnts[i]->size() > 2 && !locked(learnts[i]))
            remove(learnts[i]);
        else
            learnts[j++] = learnts[i];
    }
    for (; i < learnts.size(); i++){
        if (learnts[i]->size() > 2 && !locked(learnts[i]) && learnts[i]->activity() < extra_lim)
            remove(learnts[i]);
        else
            learnts[j++] = learnts[i];
    }
    learnts.shrink_(i - j);
}


/*_________________________________________________________________________________________________
|
|  simplifyDB : [void]  ->  [bool]
|  
|  Description:
|    Simplify all constraints according to the current top-level assigment (redundant constraints
|    may be removed altogether).
|________________________________________________________________________________________________@*/
void Solver::simplifyDB(void)
{
    if (!ok) return;    // GUARD (public method)
    assert(decisionLevel() == 0);

    if (propagate() != NULL){
        ok = false;
        return; }
    if (nAssigns() == last_simplify)
        return;

    last_simplify = nAssigns();

    for (int type = 0; type < 2; type++){
        vec<Clause*>& cs = type ? learnts : clauses;

        int     j = 0;
        for (int i = 0; i < cs.size(); i++){
            if (simplify(cs[i]))
                remove(cs[i]);
            else
                cs[j++] = cs[i];
        }
        cs.shrink_(cs.size()-j);
    }
}


/*_________________________________________________________________________________________________
|
|  search : (nof_conflicts : int) (nof_learnts : int) (params : const SearchParams&)  ->  [lbool]
|  
|  Description:
|    Search for a model the specified number of conflicts, keeping the number of learnt clauses
|    below the provided limit. NOTE! Use negative value for 'nof_conflicts' or 'nof_learnts' to
|    indicate infinity.
|  
|  Output:
|    'l_True' if a partial assigment that is consistent with respect to the clauseset is found. If
|    all variables are decision variables, this means that the clause set is satisfiable. 'l_False'
|    if the clause set is unsatisfiable. 'l_Undef' if the bound on number of conflicts is reached.
|________________________________________________________________________________________________@*/
lbool Solver::search(int nof_conflicts, int nof_learnts, const SearchParams& params)
{
    if (!ok) return l_False;    // GUARD (public method)
    assert(root_level == decisionLevel());

    stats.starts++;
    int     conflictC = 0;
    var_decay = 1 / params.var_decay;
    cla_decay = 1 / params.clause_decay;
    model.clear();

    for (;;){
        Clause* confl = propagate();
        if (confl != NULL){
            // CONFLICT

            /*EXPERIMENTAL*/trail_copy.clear();
            stats.conflicts++; conflictC++;
            vec<Lit>    learnt_clause;
            int         backtrack_level;
            if (decisionLevel() == root_level)
                return l_False;
            analyze(confl, learnt_clause, backtrack_level);
            assert(backtrack_level < decisionLevel());
            cancelUntil(max(backtrack_level, root_level));
            record(learnt_clause);
            varDecayActivity(); claDecayActivity();

        }else{
            // NO CONFLICT

            if (nof_conflicts >= 0 && conflictC >= nof_conflicts){
                // Reached bound on number of conflicts:
                progress_estimate = progressEstimate();
                cancelUntil(root_level);
                return l_Undef; }

            if (decisionLevel() == 0)
                // Simplify the set of problem clauses:
                simplifyDB(), assert(ok);

            if (nof_learnts >= 0 && learnts.size()-nAssigns() >= nof_learnts)
                // Reduce the set of learnt clauses:
                reduceDB();

            // New variable decision:
            stats.decisions++;

            /*EXPERIMENTAL*/
            Lit pick = lit_Undef;
#if 0
            while (trail_copy.size() > 0){
                pick = trail_copy.last(), trail_copy.pop();
                if (value(pick) == l_False){
                    pick = lit_Undef;
                    trail_copy.clear();
                    break;
                }else if (value(pick) == l_Undef){
                    // Decide according to trail copy:
                    check(assume(pick));
                }
            }
#endif
            /*END*/

            if (pick == lit_Undef){
                Var next = order.select(params.random_var_freq);

                if (next == var_Undef){
                    // Model found:
                    model.growTo(nVars());
                    for (int i = 0; i < nVars(); i++) model[i] = value(i);
                    /*EXPERIMENTAL*/
#if 0
                    assert(trail_copy.size() == 0);
                    for (int i = trail_lim.size()-1; i >= 0; i--)
                        trail_copy.push(trail[trail_lim[i]]);
#endif
                    /*END*/
                    cancelUntil(root_level);
                    return l_True;
                }

                if (polarity_sug[next] == toInt(l_False))
                    check(assume(~Lit(next)));
                else if (polarity_sug[next] == toInt(l_True))
                    check(assume(Lit(next)));
                else
                    check(assume(~Lit(next)));  // Arbitrarly default to negative polarity...
            }
        }
    }
}


// Return search-space coverage. Not extremely reliable.
//
double Solver::progressEstimate(void)
{
    double  progress = 0;
    double  F = 1.0 / nVars();
    for (int i = 0; i < nVars(); i++)
        if (value(i) != l_Undef)
            progress += pow(F, level[i]);
    return progress / nVars();
}


// Divide all variable activities by 1e100.
//
void Solver::varRescaleActivity(void)
{
    for (int i = 0; i < nVars(); i++)
        activity[i] *= 1e-100;
    var_inc *= 1e-100;
}


// Divide all constraint activities by 1e100.
//
void Solver::claRescaleActivity(void)
{
    for (int i = 0; i < learnts.size(); i++)
        learnts[i]->activity() *= 1e-20;
    cla_inc *= 1e-20;
}


/*_________________________________________________________________________________________________
|
|  solve : (assumps : const vec<Lit>&)  ->  [bool]
|  
|  Description:
|    Top-level solve. If using assumptions (non-empty 'assumps' vector), you must call
|    'simplifyDB()' first to see that no top-level conflict is present (which would put the solver
|    in an undefined state).
|________________________________________________________________________________________________@*/
bool Solver::solve(const vec<Lit>& assumps)
{
    simplifyDB();
    if (!ok) return false;

    SearchParams    params(0.95, 0.999, 0.02);
    double  nof_conflicts = 100;
    double  nof_learnts   = nClauses() / 3;
    //double  nof_learnts   = 4000;
    lbool   status        = l_Undef;

    for (int i = 0; i < assumps.size(); i++)
        if (!assume(assumps[i]) || propagate() != NULL){
            cancelUntil(0);
            return false; }
    root_level = decisionLevel();

    if (verbosity >= 1){
        reportf("==================================[MINISAT+]==================================\n");
        reportf("| %-9s | %-16s | %-32s | %-8s |\n", "Conflicts", "Original", "Learnt", "Progress");
        reportf("| %9s | %7s %8s | %7s %7s %8s %7s | %8s |\n","", "Clauses","Literals", "Max", "Clauses", "Literals", "LPC", "");
        reportf("==============================================================================\n");
    }

    while (status == l_Undef){
        if (verbosity >= 1){
            reportf("| %9d | %7d %8d | %7d %7d %8d %7.1f | %6.3f %% |\n",(int)stats.conflicts,(int)stats.clauses, (int)stats.clauses_literals,(int)nof_learnts, (int)stats.learnts, (int)stats.learnts_literals,(double)stats.learnts_literals / (double)stats.learnts,progress_estimate*100);
            fflush(stdout);
        }
        status = search((int)nof_conflicts, (int)nof_learnts, params);
        nof_conflicts *= 1.5;
        nof_learnts   *= 1.1;
    }
    if (verbosity >= 1)
        reportf("==============================================================================\n");

    cancelUntil(0);
    return status == l_True;
}


//=================================================================================================
// Debug:


void Solver::exportClauses(cchar* filename, vec<cchar*>& index2name, int n_splits)
{
    assert(decisionLevel() == 0);
    FILE*   out = fopen(filename, "wb"); assert(out != NULL);

    // HACK: Find biggest variable index used and count the number of clauses:
    int     n_vars = -1, n_clauses = 0;
    for (int i = 0; i < assigns.size(); i++)
        if (value(i) != l_Undef && level[i] == 0 && reason[i].isNull())
            n_vars = i+1, n_clauses++;
    for (int i = 0; i < clauses.size(); i++){
        Clause& c = *clauses[i];
        for (int j = 0; j < c.size(); j++){
            if (var(c[j])+1 > n_vars)
                n_vars = var(c[j])+1; }
        n_clauses++;
    }
    fprintf(out, "%d %d\n", n_vars + 1, n_clauses);

    for (int i = 0; i < index2name.size() - n_splits; ++i)
      fprintf(out, "%s ", index2name[i]);
    fprintf(out, "\n");

    // Export CNF:
    for (int i = 0; i < assigns.size(); i++)
        if (value(i) != l_Undef && level[i] == 0 && reason[i].isNull())
            fprintf(out, "%d 0\n", (value(i) == l_True) ? i+1 : -(i+1));

    for (int i = 0; i < clauses.size(); i++){
        Clause& c = *clauses[i];
        for (int j = 0; j < c.size(); j++)
            fprintf(out, "%s%d ", sign(c[j])?"-":"", var(c[j])+1);
        fprintf(out, "0\n");
    }
    fclose(out);
}

}// end namespace MiniSat
